Search Results

Documents authored by Schubert, Aleksy

Document
DOI: 10.4230/LIPIcs.TYPES.2016.8
Coq Support in HAHA

Authors: Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
HAHA is a tool that helps in teaching and learning Hoare logic. It is targeted at an introductory course on software verification. We present a set of new features of the HAHA verification environment that exploit Coq. These features are (1) generation of verification conditions in Coq so that they can be explored and proved interactively and (2) compilation of HAHA programs into CompCert certified compilation tool-chain. With the interactive Coq proving support we obtain an interesting functionality that makes it possible to carefully examine step-by-step verification conditions and systematically discover flaws in their formulation. As a result Coq back-end serves as a kind of specification debugger.
Cite as

Jacek Chrzaszcz, Aleksy Schubert, and Jakub Zakrzewski. Coq Support in HAHA. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 8:1-8:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{chrzaszcz_et_al:LIPIcs.TYPES.2016.8,
  author =	{Chrzaszcz, Jacek and Schubert, Aleksy and Zakrzewski, Jakub},
  title =	{{Coq Support in HAHA}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{8:1--8:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.8},
  URN =		{urn:nbn:de:0030-drops-98562},
  doi =		{10.4230/LIPIcs.TYPES.2016.8},
  annote =	{Keywords: Hoare logic, program verification, Coq theorem prover, teaching}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.12
Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic

Authors: Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Curry-Howard isomorphism makes it possible to obtain functional programs from proofs in logic. We analyse the problem of program synthesis for ML programs with algebraic types and relate it to the proof search problems in appropriate logics. The problem of synthesis for closed programs is easily equivalent to the proof construction in intuitionistic propositional logic and thus fits in the class of PSPACE-complete problems. We focus further attention on the synthesis problem relative to a given external library of functions. It turns out that the problem is undecidable for unbounded instantiation in ML. However its restriction to instantiations with atomic types only results in a case equivalent to proof search in a restricted fragment of intuitionistic first-order logic, being the core of Sigma_1 level of the logic in the Mints hierarchy. This results in EXPSPACE-completeness for this special case of the ML program synthesis problem.
Cite as

Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz. Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{benke_et_al:LIPIcs.FSCD.2016.12,
  author =	{Benke, Marcin and Schubert, Aleksy and Walukiewicz-Chrzaszcz, Daria},
  title =	{{Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.12},
  URN =		{urn:nbn:de:0030-drops-59765},
  doi =		{10.4230/LIPIcs.FSCD.2016.12},
  annote =	{Keywords: ML, program synthesis}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2014.251
Restricted Positive Quantification Is Not Elementary

Authors: Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz

Published in: LIPIcs, Volume 39, 20th International Conference on Types for Proofs and Programs (TYPES 2014)

Abstract
We show that a restricted variant of constructive predicate logic with positive (covariant) quantification is of super-elementary complexity. The restriction is to limit the number of eigenvariables used in quantifier introductions rules to a reasonably usable level. This construction suggests that the known non-elementary decision algorithms for positive logic may actually be best possible.
Cite as

Aleksy Schubert, Pawel Urzyczyn, and Daria Walukiewicz-Chrzaszcz. Restricted Positive Quantification Is Not Elementary. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 251-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schubert_et_al:LIPIcs.TYPES.2014.251,
  author =	{Schubert, Aleksy and Urzyczyn, Pawel and Walukiewicz-Chrzaszcz, Daria},
  title =	{{Restricted Positive Quantification Is Not Elementary}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{251--273},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2014.251},
  URN =		{urn:nbn:de:0030-drops-55002},
  doi =		{10.4230/LIPIcs.TYPES.2014.251},
  annote =	{Keywords: constructive logic, complexity, automata theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.128
Automata Theoretic Account of Proof Search

Authors: Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automata-theoretic model for inhabitant search, which can be viewed as proof search by the Curry-Howard isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata.
Cite as

Aleksy Schubert, Wil Dekkers, and Henk P. Barendregt. Automata Theoretic Account of Proof Search. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 128-143, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{schubert_et_al:LIPIcs.CSL.2015.128,
  author =	{Schubert, Aleksy and Dekkers, Wil and Barendregt, Henk P.},
  title =	{{Automata Theoretic Account of Proof Search}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{128--143},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.128},
  URN =		{urn:nbn:de:0030-drops-54113},
  doi =		{10.4230/LIPIcs.CSL.2015.128},
  annote =	{Keywords: simple types, automata, trees, languages of proofs}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2013
LIPIcs, Volume 26, TYPES'13, Complete Volume

Authors: Ralph Matthes and Aleksy Schubert

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
LIPIcs, Volume 26, TYPES'13, Complete Volume
Cite as

19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Proceedings{matthes_et_al:LIPIcs.TYPES.2013,
  title =	{{LIPIcs, Volume 26, TYPES'13, Complete Volume}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013},
  URN =		{urn:nbn:de:0030-drops-46370},
  doi =		{10.4230/LIPIcs.TYPES.2013},
  annote =	{Keywords: Applicative (Functional) Programming, Software/Program Verification, Specifying and Verifying and Reasoning about Programs, Mathematical Logic}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2013.i
Frontmatter, Table of Contents, Preface, Conference Organization

Authors: Ralph Matthes and Aleksy Schubert

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract
Frontmatter, Table of Contents, Preface, Conference Organization
Cite as

19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. i-x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{matthes_et_al:LIPIcs.TYPES.2013.i,
  author =	{Matthes, Ralph and Schubert, Aleksy},
  title =	{{Frontmatter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{i--x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.i},
  URN =		{urn:nbn:de:0030-drops-46225},
  doi =		{10.4230/LIPIcs.TYPES.2013.i},
  annote =	{Keywords: Frontmatter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.190
Decidable structures between Church-style and Curry-style

Authors: Ken-etsu Fujita and Aleksy Schubert

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
It is well-known that the type-checking and type-inference problems are undecidable for second order lambda-calculus in Curry-style, although those for Church-style are decidable. What causes the differences in decidability and undecidability on the problems? We examine crucial conditions on terms for the (un)decidability property from the viewpoint of partially typed terms, and what kinds of type annotations are essential for (un)decidability of type-related problems. It is revealed that there exists an intermediate structure of second order lambda-terms, called a style of hole-application, between Church-style and Curry-style, such that the type-related problems are decidable under the structure. We also extend this idea to the omega-order polymorphic calculus F-omega, and show that the type-checking and type-inference problems then become undecidable.
Cite as

Ken-etsu Fujita and Aleksy Schubert. Decidable structures between Church-style and Curry-style. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 190-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fujita_et_al:LIPIcs.RTA.2013.190,
  author =	{Fujita, Ken-etsu and Schubert, Aleksy},
  title =	{{Decidable structures between Church-style and Curry-style}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{190--205},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.190},
  URN =		{urn:nbn:de:0030-drops-40629},
  doi =		{10.4230/LIPIcs.RTA.2013.190},
  annote =	{Keywords: 2nd-order lambda-calculus, type-checking, type-inference, Church-style and Curry-style}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.198
ML with PTIME complexity guarantees

Authors: Jacek Chrzaszcz and Aleksy Schubert

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Implicit Computational Complexity is a line of research where the possibility to inference a valid property for a program implies that the program runs in particular complexity class. Soft type systems are one of the research threads within the field. We present here a soft type system with ML-like polymorphism that enjoys decidable typechecking, type inference and typability problems and gives polynomial time computational guarantees for the running time of typed programs.
Cite as

Jacek Chrzaszcz and Aleksy Schubert. ML with PTIME complexity guarantees. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 198-212, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{chrzaszcz_et_al:LIPIcs.CSL.2012.198,
  author =	{Chrzaszcz, Jacek and Schubert, Aleksy},
  title =	{{ML with PTIME complexity guarantees}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{198--212},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.198},
  URN =		{urn:nbn:de:0030-drops-36738},
  doi =		{10.4230/LIPIcs.CSL.2012.198},
  annote =	{Keywords: implicit computational complexity, polymorphism, soft type assignment}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.103
The Undecidability of Type Related Problems in Type-free Style System F

Authors: Ken-Etsu Fujita and Aleksy Schubert

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We consider here a number of variations on the System F, that are predicative second-order systems whose terms are intermediate between the Curry style and Church style. The terms here contain the information on where the universal quantifier elimination and introduction in the type inference process must take place, which is similar to Church forms. However, they omit the information on which types are involved in the rules, which is similar to Curry forms. In this paper we prove the undecidability of the type-checking, type inference and typability problems for the system. Moreover, the proof works for the predicative version of the system with finitely stratified polymorphic types. The result includes the bounds on the Leivant’s level numbers for types used in the instances leading to the undecidability.
Cite as

Ken-Etsu Fujita and Aleksy Schubert. The Undecidability of Type Related Problems in Type-free Style System F. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 103-118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{fujita_et_al:LIPIcs.RTA.2010.103,
  author =	{Fujita, Ken-Etsu and Schubert, Aleksy},
  title =	{{The Undecidability of Type Related Problems in Type-free Style System F}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{103--118},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.103},
  URN =		{urn:nbn:de:0030-drops-26475},
  doi =		{10.4230/LIPIcs.RTA.2010.103},
  annote =	{Keywords: Lambda calculus and related systems, type checking, typability, partial type inference, 2nd order unification, undecidability, Curry style type system}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact